from z3 import *

x = Int("x")
y = Int("y")
# 全称量词的示例
solve([y == x + 1, ForAll([y], Implies(y <= 0, x > y))])
# > [x = 2, y = 3]

# Lambda绑定
Z = IntSort()
B = BoolSort()
z = Int("z")
m, m1 = Array("m", Z, Z), Array("m1", Z, Z)


def memset(lo, hi, y, m):
    return Lambda([x], If(And(lo <= x, x <= hi), y, Select(m, x)))


solve([m1 == memset(1, 700, z, m), Select(m1, 6) != z])
# > no solution

# 下面的例子是可证明的
Q = Array("Q", Z, B)
prove(Implies(ForAll(Q, Implies(Select(Q, x), Select(Q, y))), x == y))
# > proved
